Previous | 
Home
Section: Partnerships and Cooperations
International Initiatives
Inria Associate Teams
POLYCORE
International Partner (Institution - Laboratory - Researcher):
See also: http://www.irisa.fr/espresso/Polycore
Inria Associate Project POLYCORE starts from an observation that can be shared with anyone how experienced with multi-threaded programming, to acknowledge the difficulty of designing and implementing such software. Resolving concurrency, synchronization, and coordination issues, and tackling the non-determinism germane in multi-threaded software is extremely difficult. Ensuring correctness with respect to the specification and deterministic behavior is however necessary for safe execution of such code on embedded architectures. It is therefore desirable to synthesize multi-threaded code from formal specifications using a provably `correct-by-construction' approach.
While time-triggered programming model simplifies code generation, our shared intuition is that multi-rate event driven execution models are much more efficiently adapted to tackle embedded software design challenges posed by forthcoming heterogeneous multi-core embedded architectures. To this aim, we develop formal models, methods, algorithms and techniques for generating provably correct multi-threaded reactive real-time embedded software for mission-critical applications. For scalable modeling of larger embedded software systems, the specification formalism has to be compositional and hierarchical.
Our proposed formalism entails a model of computation (MoC) based on a multi-rate synchronous data-flow paradigm: Polychrony. It aims at combining the capabilities of Esterel/Quartz (ESG/TUKL) for correctly programming synchronous modules, with the capabilities of Polychrony (Inria), to give high-level abstractions of complex multi-clocked networks and yet provide powerful communication and scheduling code synthesis, all combined in an application-specific modeling and programming environment, design in collaboration with Virginia Tech and the AFRL [12] , [11] . This year, we laid novel semantical foundations to designing our envisioned environment by defining a constructive semantic encompassing the polychronous data-flow model of Signal and the reactive synchronous imperative model of Quartz, and allowing to formulate the very first executable, small-step, structured operational semantics of Signal [17] .